COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00028 ENDMK
C⊗;

function syn
 (1 1 1 0 0)

syn(speci, target, envinit, program, newenv) ←
	firstsym(speci, nxtsym, spec), 
	int(nxtsym, spec, envinit, int-prog, newenv), 
	trans(int-prog, newenv, target, program).


function int
 (1 1 1 0 0)

int('function, spec, oldenv, int-prog, newenv) ← fun-spec(spec, oldenv, int-prog, newenv)
int('type, spec, oldenv, int-prog, newenv) ← type-spec(spec, oldenv, int-prog, newenv)
int('generic, spec, oldenv, int-prog, newenv) ← gen-spec(spec, oldenv, int-prog, newenv).



function fun-spec
 (1 1 0 0)

fun-spec(spec, oldenv, list('function, name, inpat, params, precond, postcond, body), 
		newenv) ←
	firstsym(spec, name, more2),
	write("input-pattern?"), firstexp(more2, inpat, more3),
	write("parameter list?"), firstexp(more3, params, more4),
	write("precondition?"), is-disjunct(more4, precond, more5),
	write("postcondition?"), is-disjunct(more5, postcond, more6),
	addfun(oldenv, name, newenv),
	write("body?"), is-body(more6, body, moren, undef, newenv, inpat).


function is-disjunct
 (1 0 0)

is-disjunct(spec, disj, more) ←
	is-conjunct(spec, conj, more1, nxtsym),
	finish-disj(more1, nxtsym, conj, disj, more).


function finish-disj
(1 1 1 0 0)

finish-disj(spec, '∨, conj, list('∨, conj, disj), more) ←
	is-disjunct(spec, disj, more)
finish-disj(spec, '/., conj, conj, spec).


function is-conjunct
 (1 0 0 0)

is-conjunct(spec, conj, more, nxtsym) ←
	firstsym(spec, litsym, more1),
	is-literal(litsym, more1, lit, more2, midsym),
	finish-conj(more2, midsym, lit, conj, more, nxtsym).


function finish-conj
(1 1 1 0 0 0)

finish-conj(spec, '∧, lit, list('∧, lit, conj), more, nxtsym) ←
	is-conjunct(spec, conj, more, nxtsym)
finish-conj(spec, '/., lit, lit, spec, '/.).



function is-literal 
 (1 1 0 0 0)

is-literal('TRUE, spec, T, more, nxtsym) ← firstsym(spec, nxtsym, more)
is-literal('T, spec, T, more, nxtsym) ← firstsym(spec, nxtsym, more)
is-literal('/(, spec, disj, more, nxtsym) ← is-disjunct(spec, disj, more1), 
	firstsym(more1, '/), more2), firstsym(more2, nxtsym, more)
is-literal(name, spec, atmf, more, nxtsym) ← firstsym(spec, '/(, more1),
	is-funapp(name, more1, atmf, more, nxtsym).


function is-funapp
 (1 1 0 0 0)

is-funapp(name, spec, cons(name, arglist), more, nxtsym) ←
	is-arglist(spec, arglist, more, nxtsym).


function is-arglist
 (1 0 0 0)

is-arglist(spec, arglist, more, nxtsym) ←
	firstsym(spec, argsym, more2),
	read-args(argsym, more2, arglist, more,nxtsym).


function read-args
 (1 1 0 0 0)

read-args('/), spec, (), more, nxtsym) ← firstsym(spec, nxtsym, more)
read-args(argsym, spec, cons(arg,arglist), more, nxtsym) ←
	is-arg(argsym, spec, arg, more1, midsym), 
	read-args(midsym, more1, arglist, more, nxtsym).


function is-arg
 (1 1 0 0 0)

is-arg(argsym, spec, const, more, nxtsym) ← is-constnt(argsym, spec, const, more1),
	firstsym(more1, nxtsym, more)
is-arg(name, spec, arg, more, lastsym) ← firstsym(spec, nxtsym, more1),
	finish-arg(nxtsym, name, more1, arg, more, lastsym).


function finish-arg
(1 1 1 0 0 0)

finish-arg('/(, name, spec, fnapp, more, nxtsym) ←
	is-funapp(name, spec, fnapp, more, nxtsym)
finish-arg(nxtsym, name, spec, name, spec, nxtsym).


function is-constnt
 (1 1 0 0)

is-constnt('/', spec, list('quote,exp), more) ←
	firstexp(spec, exp, more)
is-constnt(number, spec, number, more) ← integer(number)
is-constnt(number, spec, number, more) ← real(number)
is-constnt('undef, spec, undef, more) 
is-constnt('false, spec, false, more) 
is-constnt('true, spec, t, more) 
is-constnt('t, spec, t, more) 
is-constnt('/(, spec, (), more) ← firstsym(spec,'/),more).


function is-body
 (1 0 0 1 1 1)

is-body(spec,cons('bktrkcond,alternatives),more,genflag,env,inpat) ←
	firstsym(spec, sym, more1),
	is-hornclauses(sym, more1,alternatives,more,genflag,env,inpat).


function is-hornclauses
 (1 1 0 0 1 1 1)

is-hornclauses('/., spec,(),more,genflag,env,inpat) 
is-hornclauses(name, spec, cons(match-try-pair,alternatives),
					more,genflag,env,inpat) ←
	firstsym(spec, '/(, spec2),
	is-hclause(name,spec2,match-try-pair,more1,genflag,env,inpat,nxtsym),
	is-hornclauses(nxtsym,more1,alternatives,more,genflag,env,inpat).



function is-hclause
 (1 1 0 0 1 1 1 0)

is-hclause(name,spec,list(arglist,trylist),more,genflag,env,inpat,lastsym) ←
	is-funapp(name,spec,cons(name,arglist),more1,nxtsym),
	finish-hclause(nxtsym, name, arglist, inpat, genflag, env, more1,
					 trylist, lastsym).


function finish-hclause
(1 1 1 1 1 1 1 0 0 0)

finish-hclause('←, name, arglist, inpat, genflag, env, spec, trylist,
							more, nxtsym) ←
	mk-known(inpat, arglist, (), knownvars),
	is-subgoalist(spec, trylist, more, env, knownvars, genflag, nxtsym)
finish-hclause(nxtsym, name, arglist, inpat, genflag, env, spec,
				cons('try, ()), spec, nxtsym).


function is-subgoalist
 (1 0 0 1 1 1 0)

is-subgoalist(spec,cons('try,cons(cons(fname,arglist),sbglist)),more,env,
			knownvars,false,lastsym) ←
	firstsym(spec,name,spec2), firstsym(spec2, '/(, spec3),
	is-funapp(name,spec3,cons(name,arglist),more1,nxtsym),
	ck-generic(name,env,arglist, knownvars,fname),
	mk-allknown(arglist,knownvars,newknownvars),
	rd-subgoals(nxtsym,more1,sbglist,more,env,newknownvars,false,lastsym)
is-subgoalist(spec,cons('try,cons(cons(name,arglist),sbglist)),more,env,
			knownvars,true,lastsym) ←
	firstsym(spec,name,spec2), firstsym(spec2, '/(, spec3),
	is-funapp(name, spec3,cons(name,arglist),more1,nxtsym),
	rd-subgoals(nxtsym,more1,sbglist,more,env,knownvars,true,lastsym).



function rd-subgoals
 (1 1 0 0 1 1 1 0)

rd-subgoals('/,,spec,cons(cons(name,arglist),sbglist),
					more,env,knownvars,true,lastsym) ←
	firstsym(spec,name,more1), firstsym( more1, '/(, more12),
	is-funapp(name,more12,cons(name,arglist),more2,nxtsym),
	rd-subgoals(nxtsym,more2,sbglist,more,env,knownvars,true,lastsym)
rd-subgoals('/,,spec,cons(cons(fname,arglist),sbglist),
					more,env,knownvars,false,lastsym) ←
	firstsym(spec,name,more1), firstsym(more1, '/(, more21),
	is-funapp(name,more21,cons(name,arglist),more2,nxtsym),
	ck-generic(name,env,arglist,knownvars,fname),
	mk-allknown(arglist,knownvars,newknownvars),
	rd-subgoals(nxtsym,more2,sbglist,more,env,newknownvars,false,lastsym)
rd-subgoals(nxtsym, spec, (), spec, env, knownvars, genflag, nxtsym) .



function ck-generic
 (1 1 1 1 0)

ck-generic(name, env, arglist, knownvars, name) ← generic(name, env, undef)
ck-generic(name, env, arglist, knownvars, fname) ←
	generic(name, env, selections),
	mk_pat(arglist, knownvars, inpat),
	choose-fun(inpat, selections, fname).



function generic
 (1 1 0)

generic(name,list(generics,functions, types), selections) ←
	findin(name,generics,selections).



function findin
 (1 1 0)

findin(name, (), 'undef)
findin(name, cons(cons(name,x),y), x)
findin(name, cons(cons(other,x),y), z) ← findin(name,y,z).



function addfun
 (1 1 0)

addfun(list(generics,functions,types),name,
		     list(generics, cons(name,functions),types)).



function not-in
 (1 1)

not-in(x,())
not-in(x,l) ← member(x,l,false).



function member
 (1 1 0)

member(x,cons(x,l),true)
member(x,cons(y,l),ans) ← member(x,l,ans)
member(x,(),false).



function mk-allknown
 (1 1 0)

mk-allknown((),knownvars,knownvars)
mk-allknown(cons(x,l), knownvars, newknownvars) ← vars_in(x,vl),
	mk-allknown(l, knownvars, nkv), append$(vl, nkv, newknownvars).



function mk-known
 (1 1 1 0)

mk-known((), (), knownvars, knownvars)
mk-known(cons(1,l), cons(x,k), knownvars, newknownvars) ← vars_in(x,vl),
	mk-known(l,k,knownvars, nkv), append$(vl, nkv, newknownvars)
mk-known(cons(0,l), cons(x,k), knownvars, newknownvars) ←
	mk-known(l, k, knownvars, newknownvars).



function vars_in
 (1 0)

vars_in(exp,()) ← itsaconstant(exp,true)
vars_in(exp, cons(exp,())) ← itsavar(exp,true)
vars_in(cons(name,arglist), varlist) ← varsinlist(arglist, varlist).



function varsinlist
 (1 0)

varsinlist((), ())
varsinlist(cons(s,l), varlist) ← vars_in(x, varlist1),
	varsinlist(l, varlist2), append$(varlist1, varlist2, varlist).


function itsaconstant
 (1 0)

itsaconstant(x, true) ← itsanumber(x, true)
itsaconstant(cons('quote,l), true)
itsaconstant(t, true)
itsaconstant('undef, true)
itsaconstant((), true)
itsaconstant('false, true) 
itsaconstant('true, true)
itsaconstant('f, true)
itsaconstant(x, true) ← is-string(x).

function itsanumber
 (1 0)

itsanumber(x,true) ← real(x)
itsanumber(x, true) ← integer(x).

function itsavar
 (1 0)

itsavar(cons(x,y), false)
itsvar(exp, true) ← itsaconstant(exp, false).



function append$
 (1 1 0)

append$(x,(),x)
append$( (), x, x)
append$(cons(x,l1), l2, cons(x,l3)) ← append$(l1, l2, l3).



function choose-fun
 (1 1 0)

choose-fun(inpat, cons(pattern, cons(fname, sels)), fname) ←
	enuf-known(inpat, pattern, true)
choose-fun(inpat, cons(pattern, cons(fname,sels)), funname) ←
	choose-fun(inpat, sels, funname)
choose-fun(inpat, (), undef).



function enuf-known
 (1 1 0)

enuf-known((), (), true)
enuf-known(cons(1,l), cons(x,k), ans) ← enuf-known(l,k,ans)
enuf-known(cons(0,l), cons(1,k), false).



function mk_pat
 (1 1 0)

mk_pat( (), knownvars, ())
mk_pat(cons(arg,l), knownvars, cons(1,k)) ←
	is-known(arg, knownvars, true), mk_pat(l, knownvars, k)
mk_pat(cons(arg,l), knownvars, cons(0,k)) ← mk_pat(l, knownvars, k).



function is-known
 (1 1 0)

is-known(x, knownvars, true) ← itsaconstant(x,true)
is-known(cons(f,l), knownvars,ans) ← known-list(l, knownvars, ans)
is-known(x, knownvars, ans) ← member(x, knownvars, ans).



function knownlist
 (1 1 0)

known-list((), knownvars, true)
known-list(cons(x,l), knownvars, true) ← is-known(x, knownvars, true),
	known-list(l,knownvars,true).



function type-spec
 (1 1 0 0)

type-spec(spec,oldenv,
		list('type,name,'(1 0), '(x y), T, '(boolean y),body), newenv) ←
	firstsym(spec, name, more1),
	add-type(oldenv, name, newenv),
	write("body?"),
	is-body(more1, body, morex, undef, newenv, '(1 0)).



function add-type
 (1 1 0)

add-type(list(generics,functions,types), name, 
			list(generics,functions, cons(name,types))).



function gen-spec
 (1 1 0 0)

gen-spec(spec, oldenv, 
		cons(list('generic, name, params, selections), deflist), newenv) ←
	firstsym(spec, name, more1),
	write("parameter list?"), firstexp(more1, params, more2),
	write("choices?"), firstsym(more2, nxtsym, more3),
	rd-choices(nxtsym, more3, choicelist, bodylist, more4),
	add-gen(oldenv, name, choicelist, newenv),
	repeats-of(bodylist, rep-bodnams),
	write("body-defs:"),
	rd-bodies(more4, choicelist, (), (), params, rep-bodnams, newenv, 
			deflist, morex).



function rd-choices
 (1 1 0 0 0)

rd-choices('/., spec, (), (), more) 
rd-choices('/(, spec, cons(list(inpat,name,precond,postcond,bodnam), choicelist), 
			cons(bodnam,bodylist), more) ←
	firstsym(spec, nxtsym, spec2),
	readinpat(nxtsym, spec2, inpat, more1), write("function name?"),
	firstsym(more1, name, more2), write("precondition?"),
	is-disjunct(more2, precond, more3),
	write("postcondition?"),
	is-disjunct(more3, postcond, more4),
	write("body name?"),
	firstsym(more4, bodnam, more5),
	write("choices?"), firstsym(more5, chsym, more6),
	rd-choices(chsym, more6, choicelist, bodylist, more).



function readinpat
 (1 1 0 0)

readinpat('/), spec, (), spec)
readinpat(digit, spec, cons(digit, restinpat), more) ←
	firstsym(spec, nxtsym, more1),
	readinpat(nxtsym, more1, restinpat, more).




function rd-bodies
 (1 1 1 1 1 1 1 0 0)

rd-bodies(spec, (), rep-bodies, donelist, params, rep-bodnams, env, (), spec)
rd-bodies(spec, cons(list(inpat,name,precond,postcond,bodnam), choicelist),
		rep-bodies, donelist, params, rep-bodnams,env,
		cons(list('function,name,inpat,params,precond,postcond,body), deflist),
		more) ←
	not-in(bodnam, donelist), not-in(bodnam,rep-bodnams),
	write(bodnam), write("?"),
	is-body(spec, body, more1, false, env, inpat),
	rd-bodies(more1, choicelist, rep-bodies, cons(bodnam,donelist), params,
			 rep-bodnams, env, deflist, more)
rd-bodies(spec, cons(list(inpat,name,precond,postcond,bodnam), choicelist),
		rep-bodies, donelist, params, rep-bodnams,env,
		cons(list('function,name,inpat,params,precond,postcond,body), deflist),
		more) ←
	member(bodnam,donelist,true),
	getb(bodnam, rep-bodies, genbody),
	spec-body(inpat, env, genbody, body)
rd-bodies(spec, cons(list(inpat,name,precond,postcond,bodnam), choicelist),
		cons(cons(bodnam,genbody),rep-bodies), donelist, params, 
			rep-bodnams,env,
		cons(list('function,name,inpat,params,precond,postcond,body), deflist),
		more) ←
	not-in(bodnam, donelist), member(bodnam, rep-bodnams, true),
	write(bodnam), write("?"),
	is-body(spec, genbody, more1, true, env, inpat),
	spec-body(inpat, env, genbody, body).



function getb
 (1 1 0)

getb(bodnam, cons(cons(bodnam,genbody), rep-bodies), genbody)
getb(bodnam, cons(x,repbodies), genbody) ←
	getb(bodnam, repbodies, genbody).


function spec-body
 (1 1 1 0)

spec-body(inpat, env, cons('bktrkcond, genalternatives), 
			cons('bktrkcond, alternatives) ) ←
	spec-alts(inpat, env, genalternatives, alternatives).



function spec-alts
 (1 1 1 0)

spec-alts(inpat, env, (), ())
spec-alts(inpat, env, cons(genmatch-try-pair, genalternatives), 
			cons(match-try-pair, alternatives)) ←
	spec-clause(inpat, env, genmatch-try-pair, match-try-pair),
	spec-alts(inpat, env, genalternatives, alternatives).



function spec-clause
 (1 1 1 0)

spec-clause(inpat, env, list(arglist, cons('try,genlist)), 
			list(arglist, cons('try,sblist))) ←
	mk-known(inpat, arglist, (), knownvars),
	spec-goalist(genlist, env, knownvars, sblist).



function spec-goalist
 (1 1 1 0)

spec-goalist((), env, knownvars, ())
spec-goalist(cons( cons(name,l), genlist), env, knownvars, 
			cons( cons(name,l),sblist)) ←
	generic(name, env, undef),
	mk-allknown(l, knownvars, newknownvars),
	spec-goalist(genlist, env, newknownvars, sblist)
spec-goalist(cons(cons(genname,arglist), genlist), env, knownvars, 
			cons(cons(name,arglist), sblist)) ←
	generic(genname, env, selections),
	mk_pat(arglist, knownvars, inpat),
	choose-fun(inpat, selections, name),
	mk-allknown(arglist,knownvars, newknownvars),
	spec-goalist(genlist, env, newkownvars, sblist).



function trans
 (1 1 1 0)

trans(list( 'function, name, inpat, params, precond, postcond,  
			cons('bktrkcond, alternatives)), env, 'lisp,
	list( 'defun, name, 'fexpr, '(l),
			list( 'cond list( list('trueprecond,list('cons,
								  list('quote, name)
								  'l)),
					  list('bktrkcond, 'l, list('quote,
								    alternatives))),
				    '(t 'undef))) ).
.